Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    minus(0,Y)  → 0
2:    minus(s(X),s(Y))  → minus(X,Y)
3:    geq(X,0)  → true
4:    geq(0,s(Y))  → false
5:    geq(s(X),s(Y))  → geq(X,Y)
6:    div(0,s(Y))  → 0
7:    div(s(X),s(Y))  → if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
8:    if(true,X,Y)  → X
9:    if(false,X,Y)  → Y
There are 6 dependency pairs:
10:    MINUS(s(X),s(Y))  → MINUS(X,Y)
11:    GEQ(s(X),s(Y))  → GEQ(X,Y)
12:    DIV(s(X),s(Y))  → IF(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
13:    DIV(s(X),s(Y))  → GEQ(X,Y)
14:    DIV(s(X),s(Y))  → DIV(minus(X,Y),s(Y))
15:    DIV(s(X),s(Y))  → MINUS(X,Y)
The approximated dependency graph contains 2 SCCs: {11} and {10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006